|
A parity game is played on a colored directed graph, where each node has been colored by a priority – one of (usually) finitely many natural numbers. Two players, 0 and 1, move a (single, shared) token along the edges of the graph. The owner of the node that the token falls on selects the successor node, resulting in a (possibly infinite) path, called the play. The winner of a finite play is the player whose opponent is unable to move. The winner of an infinite play is determined by the priorities appearing in the play. Typically, player 0 wins an infinite play if the largest priority that occurs infinitely often in the play is even. Player 1 wins otherwise. This explains the word "parity" in the title. Parity games lie in the third level of the borel hierarchy, and are consequently determined.〔D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363–371 (1975)〕 Games related to parity games were implicitly used in Rabin's proof of decidability of second order theory of n successors, where determinacy of such games was proven. The Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games.〔E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0〕 Moreover, parity games are history-free determined.〔〔A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)〕 This means that if a player has a winning strategy then that player has a winning strategy that depends only on the current board position, and not on the history of the play. ==Solving a game== ''Solving'' a parity game played on a finite graph means deciding, for a given starting position, which of the two players has a winning strategy. It has been shown that this problem is in NP and Co-NP, as well as UP and co-UP.〔Grädel 2007, p. 163〕 It remains an open question whether this decision problem is solvable in PTime. Given that parity games are history-free determined, solving a given parity game is equivalent to solving the following simple looking graph-theoretic problem. Given a finite colored directed bipartite graph with ''n'' vertices , and ''V'' colored with colors from ''1'' to ''m'', is there a choice function selecting a single out-going edge from each vertex of , such that the resulting subgraph has the property that in each cycle the largest occurring color is even. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「parity game」の詳細全文を読む スポンサード リンク
|